\batchmode
\makeatletter
\def\input@path{{/Users/sergei.winitzki/Code/talks/ftt-fp/}}
\makeatother
\documentclass[english,,russian]{beamer}
\usepackage[T2A,T1]{fontenc}
\usepackage[utf8]{inputenc}
\setcounter{secnumdepth}{3}
\setcounter{tocdepth}{3}
\usepackage{babel}
\usepackage{tipa}
\usepackage{tipx}
\usepackage{amsmath}
\usepackage{wasysym}
\usepackage[all]{xy}
\ifx\hypersetup\undefined
  \AtBeginDocument{%
    \hypersetup{unicode=true,pdfusetitle,
 bookmarks=true,bookmarksnumbered=false,bookmarksopen=false,
 breaklinks=false,pdfborder={0 0 1},backref=false,colorlinks=true}
  }
\else
  \hypersetup{unicode=true,pdfusetitle,
 bookmarks=true,bookmarksnumbered=false,bookmarksopen=false,
 breaklinks=false,pdfborder={0 0 1},backref=false,colorlinks=true}
\fi

\makeatletter

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% LyX specific LaTeX commands.
\DeclareRobustCommand{\cyrtext}{%
  \fontencoding{T2A}\selectfont\def\encodingdefault{T2A}}
\DeclareRobustCommand{\textcyr}[1]{\leavevmode{\cyrtext #1}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Textclass specific LaTeX commands.
% this default might be overridden by plain title style
\newcommand\makebeamertitle{\frame{\maketitle}}%
% (ERT) argument for the TOC
\AtBeginDocument{%
  \let\origtableofcontents=\tableofcontents
  \def\tableofcontents{\@ifnextchar[{\origtableofcontents}{\gobbletableofcontents}}
  \def\gobbletableofcontents#1{\origtableofcontents}
}
\newenvironment{lyxcode}
  {\par\begin{list}{}{
    \setlength{\rightmargin}{\leftmargin}
    \setlength{\listparindent}{0pt}% needed for AMS classes
    \raggedright
    \setlength{\itemsep}{0pt}
    \setlength{\parsep}{0pt}
    \normalfont\ttfamily}%
   \def\{{\char`\{}
   \def\}{\char`\}}
   \def\textasciitilde{\char`\~}
   \item[]}
  {\end{list}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% User specified LaTeX commands.
\usetheme[secheader]{Boadilla}
\usecolortheme{seahorse}
\title[Chapter 10: Free type constructions]{Chapter 10: Free type constructions}
%\subtitle{Part 2: Their laws and structure}
\author{Sergei Winitzki}
\date{2018-11-22}
\institute[ABTB]{Academy by the Bay}
\setbeamertemplate{headline}{} % disable headline at top
\setbeamertemplate{navigation symbols}{} % disable navigation bar at bottom
\usepackage[all]{xy}
\usepackage[nocenter]{qtree}
\makeatletter
% Macros to assist LyX with XYpic when using scaling.
\newcommand{\xyScaleX}[1]{%
\makeatletter
\xydef@\xymatrixcolsep@{#1}
\makeatother
} % end of \xyScaleX
\makeatletter
\newcommand{\xyScaleY}[1]{%
\makeatletter
\xydef@\xymatrixrowsep@{#1}
\makeatother
} % end of \xyScaleY
\newcommand{\shui}{\begin{CJK}{UTF8}{gbsn}水\end{CJK}}
\usepackage{CJKutf8} % For occasional Chinese characters. Also, add "russian" to documentclass.

\makeatother

\begin{document}
\frame{\titlepage}
\begin{frame}{The interpreter pattern I. Expression trees}

Main idea: Represent a program as a data structure, run it later
\begin{itemize}
\item Example: a simple DSL for complex numbers
\end{itemize}
\vspace{-0.35cm}%
\begin{minipage}[t]{0.35\columnwidth}%
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}val~a~=~\textquotedbl 1+2{*}i\textquotedbl .toComplex}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}val~b~=~a~{*}~\textquotedbl 3-4{*}i\textquotedbl .toComplex}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}b.conj}{\footnotesize\par}
\end{lyxcode}
%
\end{minipage}\hspace*{\fill}%
\begin{minipage}[t]{0.45\columnwidth}%
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}Conj(}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~Mul(}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~~Str(\textquotedbl 1+2{*}i\textquotedbl ),~Str(\textquotedbl 3-4{*}i\textquotedbl )}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}))}{\footnotesize\par}
\end{lyxcode}
%
\end{minipage}\hspace*{\fill}
\begin{itemize}
\item \emph{Unevaluated} operations \texttt{\textcolor{blue}{\footnotesize{}Str}},
\texttt{\textcolor{blue}{\footnotesize{}Mul}}, \texttt{\textcolor{blue}{\footnotesize{}Conj}}
are defined as case classes:
\end{itemize}
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}sealed~trait~Prg}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Str(s:~String)~extends~Prg}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Mul(p1:~Prg,~p2:~Prg)~extends~Prg}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Conj(p:~Prg)~extends~Prg}{\footnotesize\par}
\end{lyxcode}
\begin{itemize}
\item An \emph{interpreter} will ``run'' the program and return a complex
number
\end{itemize}
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}def~run(prg:~Prg):~(Double,~Double)~=~...}{\footnotesize\par}
\end{lyxcode}
\begin{itemize}
\item Benefits: programs are data, can compose \& transform before running
\item Shortcomings: this DSL works only with simple expressions
\begin{itemize}
\item Cannot represent variable binding and conditional computations
\item Cannot use any non-DSL code (e.g.~a numerical algorithms library)
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{The interpreter pattern II. Variable binding}

\vspace{-0.1cm}A DSL with variable binding and conditional computations
\begin{itemize}
\item Example: imperative API for reading and writing files
\begin{itemize}
\item Need to bind a \emph{non-DSL variable} to a value computed by DSL
\item Later, need to use that non-DSL variable in DSL expressions
\item The rest of the DSL program is a (Scala) function of that variable
\end{itemize}
\end{itemize}
\vspace{-0.15cm}%
\begin{minipage}[t]{0.35\columnwidth}%
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}val~p~=~path(\textquotedbl /file\textquotedbl )}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}val~str:~String~=~read(p)}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}if~(str.nonEmpty)}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~read(path(str))}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}else~\textquotedbl Error:~empty~path\textquotedbl}{\footnotesize\par}
\end{lyxcode}
%
\end{minipage}\hspace*{\fill}%
\begin{minipage}[t]{0.45\columnwidth}%
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}Bind(}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~Read(Path(Literal(\textquotedbl /file\textquotedbl ))),}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~\{~str~$\Rightarrow$}\textcolor{darkgray}{\footnotesize{}~//~read~value~`str`}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~~~if~(str.nonEmpty)}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~~~~~Read(Path(Literal(str)))}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~~~else~Literal(\textquotedbl Error:~empty~path\textquotedbl )}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~\})}{\footnotesize\par}
\end{lyxcode}
%
\end{minipage}\hspace*{\fill}
\begin{itemize}
\item \vspace{0.1cm}Unevaluated operations are implemented via case classes:
\end{itemize}
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}sealed~trait~Prg}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Bind(p:~Prg,~f:~String~$\Rightarrow$~Prg)~extends~Prg~}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Literal(s:~String)~extends~Prg~}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Path(s:~Prg)~extends~Prg}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Read(p:~Prg)~extends~Prg}{\footnotesize\par}
\end{lyxcode}
\begin{itemize}
\item \vspace{-0.1cm}Interpreter: \texttt{\textcolor{blue}{\footnotesize{}def
run(prg: Prg): String = ...}} 
\end{itemize}
\end{frame}

\begin{frame}{The interpreter pattern III. Type safety}
\begin{itemize}
\item So far, the DSL has no type safety: every value is a \texttt{\textcolor{blue}{\footnotesize{}Prg}} 
\begin{itemize}
\item We want to avoid errors, e.g. \texttt{\textcolor{blue}{\footnotesize{}Read(Read(...))}}
should not compile
\end{itemize}
\item Let \texttt{\textcolor{blue}{\footnotesize{}Prg{[}A{]}}} denote a
DSL program returning value of type \texttt{\textcolor{blue}{\footnotesize{}A}}
\emph{when run}:
\end{itemize}
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}sealed~trait~Prg{[}A{]}}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Bind(p:~Prg{[}String{]},~f:~String~$\Rightarrow$~Prg{[}String{]})}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~extends~Prg{[}String{]}}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Literal(s:~String)~extends~Prg{[}String{]}~}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Path(s:~Prg{[}String{]})~extends~Prg{[}nio.file.Path{]}}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Read(p:~Prg{[}nio.file.Path{]})~extends~Prg{[}String{]}}{\footnotesize\par}
\end{lyxcode}
\begin{itemize}
\item Interpreter: \texttt{\textcolor{blue}{\footnotesize{}def run(prg: Prg{[}String{]}): String
= ...}}{\footnotesize\par}
\item Our example DSL program is type-safe now:
\end{itemize}
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}val~prg:~Prg{[}String{]}~=~Bind(}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~Read(Path(Literal(\textquotedbl /file\textquotedbl ))),}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~~~~\{~str:~String~$\Rightarrow$}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~~~if~(str.nonEmpty)}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~~~~~Read(Path(Literal(str)))}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~~~else~Literal(\textquotedbl Error:~empty~path\textquotedbl )}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~\})}{\footnotesize\par}
\end{lyxcode}
\end{frame}

\begin{frame}{The interpreter pattern IV. Cleaning up the DSL}

\vspace{-0.2cm}Our DSL so far:
\begin{lyxcode}
\vspace{-0.0cm}\textcolor{blue}{\footnotesize{}sealed~trait~Prg{[}A{]}}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Bind(p:~Prg{[}String{]},~f:~String~$\Rightarrow$~Prg{[}String{]})}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~extends~Prg{[}String{]}}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Literal(s:~String)~extends~Prg{[}String{]}}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Path(s:~Prg{[}String{]})~extends~Prg{[}nio.file.Path{]}}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Read(p:~Prg{[}nio.file.Path{]})~extends~Prg{[}String{]}}{\footnotesize\par}
\end{lyxcode}
Problems with this DSL:
\begin{itemize}
\item Cannot use \texttt{\textcolor{blue}{\footnotesize{}Read(p: nio.file.Path)}},
only \texttt{\textcolor{blue}{\footnotesize{}Read(p: Prg{[}nio.file.Path{]})}} 
\item Cannot bind variables or return values other than \texttt{\textcolor{blue}{\footnotesize{}String}} 
\end{itemize}
To fix these problems, make \texttt{\textcolor{blue}{\footnotesize{}Literal}}
a fully parameterized operation and replace \texttt{\textcolor{blue}{\footnotesize{}Prg{[}A{]}}}
by \texttt{\textcolor{blue}{\footnotesize{}A}} in case class arguments
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}sealed~trait~Prg{[}A{]}}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Bind{[}A,~B{]}(p:~Prg{[}A{]},~f:~A$\Rightarrow$Prg{[}B{]})~extends~Prg{[}B{]}}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Literal{[}A{]}(a:~A)~extends~Prg{[}A{]}}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Path(s:~String)~extends~Prg{[}nio.file.Path{]}}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Read(p:~nio.file.Path)~extends~Prg{[}String{]}}{\footnotesize\par}
\end{lyxcode}
\begin{itemize}
\item \vspace{-0.0cm}The type signatures of \texttt{\textcolor{blue}{\footnotesize{}Bind}}
and \texttt{\textcolor{blue}{\footnotesize{}Literal}} are like \texttt{\textcolor{blue}{\footnotesize{}flatMap}}
and \texttt{\textcolor{blue}{\footnotesize{}pure}} 
\end{itemize}
\begin{lyxcode}
\end{lyxcode}
\end{frame}

\begin{frame}{The interpreter pattern V. Define \texttt{Monad}-like methods}
\begin{itemize}
\item \vspace{-0.3cm}We can actually define the methods \texttt{\textcolor{blue}{\footnotesize{}map}},
\texttt{\textcolor{blue}{\footnotesize{}flatMap}}, \texttt{\textcolor{blue}{\footnotesize{}pure}}:
\end{itemize}
\begin{lyxcode}
\vspace{-0.1cm}\textcolor{blue}{\footnotesize{}sealed~trait~Prg{[}A{]}~\{}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~def~flatMap{[}B{]}(f:~A~$\Rightarrow$~Prg{[}B{]}):~Prg{[}B{]}~=~Bind(this,~f)}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~def~map{[}B{]}(f:~A~$\Rightarrow$~B):~Prg{[}B{]}~=~flatMap(this,~f~andThen~Prg.pure)}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}\}}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}object~Prg~\{~def~pure{[}A{]}(a:~A):~Prg{[}A{]}~=~Literal(a)~\}}{\footnotesize\par}
\end{lyxcode}
\begin{itemize}
\item \vspace{-0.15cm}These methods don't run anything, only create unevaluated
structures
\item DSL programs can now be written as functor blocks and composed:
\end{itemize}
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}def~readPath(p:~String):~Prg{[}String{]}~=~for~\{}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~path~$\leftarrow$~Path(p)}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~str~~$\leftarrow$~Read(path)}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}\}~yield~str}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}val~prg:~Prg{[}String{]}~=~for~\{}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~str~$\leftarrow$~readPath(\textquotedbl /file\textquotedbl )}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~result~$\leftarrow$~~if~(str.nonEmpty)}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~~~~~readPath(str)}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~~~else~Prg.pure(\textquotedbl Error:~empty~path\textquotedbl )}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}\}~yield~result}{\footnotesize\par}
\end{lyxcode}
\begin{itemize}
\item \vspace{-0.15cm}Interpreter: \texttt{\textcolor{blue}{\footnotesize{}def
run{[}A{]}(prg: Prg{[}A{]}): A = ...}} 
\end{itemize}
\end{frame}

\begin{frame}{The interpreter pattern VI. Refactoring to an abstract DSL}
\begin{itemize}
\item Write a DSL for complex numbers in a similar way:
\end{itemize}
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}sealed~trait~Prg{[}A{]}~\{~def~flatMap~...~\}}\textcolor{darkgray}{\footnotesize{}~//~no~code~changes}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Bind{[}A,~B{]}(p:~Prg{[}A{]},~f:~A$\Rightarrow$Prg{[}B{]})~extends~Prg{[}B{]}}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Literal{[}A{]}(a:~A)~extends~Prg{[}A{]}}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}type~Complex~=~(Double,~Double)}\textcolor{darkgray}{\footnotesize{}~//~custom~code~starts~here}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Str(s:~String)~extends~Prg{[}Complex{]}}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Mul(c1:~Complex,~C2:~Complex)~extends~Prg{[}Complex{]}}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Conj(c:~Complex)~extends~Prg{[}Complex{]}}{\footnotesize\par}
\end{lyxcode}
\begin{itemize}
\item Refactor this DSL to separate common code from custom code:
\end{itemize}
\begin{lyxcode}
\vspace{-0.15cm}\textcolor{blue}{\footnotesize{}sealed~trait~DSL{[}F{[}\_{]},~A{]}~\{~def~flatMap~...~\}}\textcolor{darkgray}{\footnotesize{}~//~no~code~changes}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}type~Prg{[}A{]}~=~DSL{[}F,~A{]}}\textcolor{darkgray}{\footnotesize{}~//~just~for~convenience}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Bind{[}A,~B{]}(p:~Prg{[}A{]},~f:~A$\Rightarrow$Prg{[}B{]})~extends~Prg{[}B{]}}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Literal{[}A{]}(a:~A)~extends~Prg{[}A{]}}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Ops{[}A{]}(f:~F{[}A{]})~extends~Prg{[}A{]}}\textcolor{darkgray}{\footnotesize{}~//~custom~operations~here}{\footnotesize\par}
\end{lyxcode}
\begin{itemize}
\item Interpreter is parameterized by a ``value extractor'' {\footnotesize{}$\text{Ex}^{F}\equiv\forall A.\left(F^{A}\Rightarrow A\right)$}{\footnotesize\par}
\end{itemize}
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}def~run{[}F{[}\_{]},~A{]}(ex:~Ex{[}F{]})(prg:~DSL{[}F,~A{]}):~A~=~...}{\footnotesize\par}
\end{lyxcode}
\begin{itemize}
\item The constructor \texttt{\textcolor{blue}{\footnotesize{}DSL{[}F{[}\_{]},
A{]}}} is called a \textbf{free monad} over \texttt{\textcolor{blue}{\footnotesize{}F}} 
\end{itemize}
\end{frame}

\begin{frame}{The interpreter pattern VII. Handling errors}
\begin{itemize}
\item \vspace{-0.15cm}To handle errors, we want to evaluate \texttt{\textcolor{blue}{\footnotesize{}DSL{[}F{[}\_{]},
A{]}}} to \texttt{\textcolor{blue}{\footnotesize{}Either{[}Err, A{]}}} 
\item Suppose we have a value extractor of type $\text{Ex}^{F}\equiv\forall A.\left(F^{A}\Rightarrow\text{Err}+A\right)$
\item The code of the interpreter is almost unchanged:
\end{itemize}
\begin{lyxcode}
\vspace{-0.4cm}\textcolor{blue}{\footnotesize{}def~run{[}F{[}\_{]},~A{]}(extract:~Ex{[}F{]})(prg:~DSL{[}F,~A{]}):~Either{[}Err,~A{]}~=}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~prg~match~\{}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~~~case~b:~Bind{[}F,~\_,~A{]}~\ensuremath{\Rightarrow}~b~match~\{~case~Bind(p,~f)~\ensuremath{\Rightarrow}~}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~~~~~~~run(extract)(p).flatMap(f~andThen~run(extract))}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~~~\}}\textcolor{darkgray}{\footnotesize{}~~~~~//~Here,~the~.flatMap~is~from~Either.}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~~~case~Literal(a)~\ensuremath{\Rightarrow}~Right(a)}\textcolor{darkgray}{\footnotesize{}~//~pure:~A~$\Rightarrow$~Err~+~A}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~~~case~Ops(f)~\ensuremath{\Rightarrow}~extract(f)~~~~~}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}\}}{\footnotesize\par}
\end{lyxcode}
\begin{itemize}
\item \vspace{-0.15cm}The code of \texttt{\textcolor{blue}{\footnotesize{}run}}
only uses \texttt{\textcolor{blue}{\footnotesize{}flatMap}} and \texttt{\textcolor{blue}{\footnotesize{}pure}}
from \texttt{\textcolor{blue}{\footnotesize{}Either}} 
\item We can generalize to any other monad $M^{A}$ instead of \texttt{\textcolor{blue}{\footnotesize{}Either{[}Err,
A{]}}} 
\end{itemize}
The resulting construction:
\begin{itemize}
\item Start with an ``operations type constructor'' $F^{A}$ (often not
a functor)
\item Use $\text{DSL}^{F,A}$ and interpreter {\footnotesize{}$\text{run}^{M,A}:\left(\forall X.F^{X}\Rightarrow M^{X}\right)\Rightarrow\text{DSL}^{F,A}\Rightarrow M^{A}$}{\footnotesize\par}
\item Create a DSL program $\text{prg}:\text{DSL}^{F,A}$ and an extractor
$\text{ex}^{X}:F^{X}\Rightarrow M^{X}$
\item Run the program with the extractor: \texttt{\textcolor{blue}{\footnotesize{}run(ex)(prg)}};
get a value $M^{A}$
\end{itemize}
\end{frame}

\begin{frame}{The interpreter pattern VIII. Monadic DSLs: summary}
\begin{itemize}
\item \vspace{-0.15cm}Begin with a number of operations, which are typically
functions of fixed known types such as $A_{1}\Rightarrow B_{1}$,
$A_{2}\Rightarrow B_{2}$ etc.
\item Define a type constructor (typically not a functor) encapsulating
all the operations as case classes, with or without type parameters
\end{itemize}
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}sealed~trait~F{[}A{]}}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Op1(a1:~A1)~extends~F{[}B1{]}}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Op2(a1:~A2)~extends~F{[}B2{]}}{\footnotesize\par}
\end{lyxcode}
\begin{itemize}
\item Use \texttt{\textcolor{blue}{\footnotesize{}DSL{[}F,A{]}}} with this
\texttt{\textcolor{blue}{\footnotesize{}F}} to write monadic DSL programs
\texttt{\textcolor{blue}{\footnotesize{}prg:~DSL{[}F,A{]}}} 
\item Choose a target monad \texttt{\textcolor{blue}{\footnotesize{}M{[}A{]}}}
and implement an extractor \texttt{\textcolor{blue}{\footnotesize{}ex:F{[}A{]}$\Rightarrow$M{[}A{]}}} 
\item Run the program with the extractor, \texttt{\textcolor{blue}{\footnotesize{}val
res:~M{[}A{]} = run(ex)(prg)}} 
\end{itemize}
Further directions (out of scope for this chapter):
\begin{itemize}
\item May choose another monad \texttt{\textcolor{blue}{\footnotesize{}N{[}A{]}}}
and use interpreter \texttt{\textcolor{blue}{\footnotesize{}M{[}A{]}
$\Rightarrow$ N{[}A{]}}} 
\begin{itemize}
\item E.g.~transform into another monadic DSL to optimize, test, etc.
\end{itemize}
\item Since \texttt{\textcolor{blue}{\footnotesize{}DSL{[}F,A{]}}} has a
monad API, we can use monad transformers on it
\item Can combine two or more DSLs in a disjunction: $\text{DSL}^{F+G+H,A}$
\end{itemize}
\end{frame}

\begin{frame}{Monad laws for DSL programs}

Monad laws hold for DSL programs only after evaluating them
\begin{itemize}
\item Consider the law $\text{flm}\left(\text{pure}\right)=\text{id}$;
both functions $\text{DSL}^{F,A}\Rightarrow\text{DSL}^{F,A}$
\item Apply both sides to some $\text{prg}:\text{DSL}^{F,A}$ and get the
new value
\end{itemize}
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}prg.flatMap(pure)~==~Bind(prg,~a~$\Rightarrow$~Literal(a))}{\footnotesize\par}
\end{lyxcode}
\begin{itemize}
\item This new value is \emph{not equal} to \texttt{\textcolor{blue}{\footnotesize{}prg}},
so this monad law fails!
\begin{itemize}
\item Other laws fail as well because operations never reduce anything
\end{itemize}
\item After interpreting this program into a target monad $M^{A}$, the
law holds:
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}run(ex)(prg).flatMap((a~$\Rightarrow$~Literal(a))~andThen~run(ex))~}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~==~run(ex)(prg).flatMap(a~$\Rightarrow$~run(ex)(Literal(a))~}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~==~run(ex)(prg).flatMap(a~$\Rightarrow$~pure(a))}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~==~run(ex)(prg)}{\footnotesize\par}
\end{lyxcode}
\begin{itemize}
\item Here we have assumed that the laws hold for $M^{A}$
\item All other laws also hold after interpreting into a lawful monad $M^{A}$
\end{itemize}
\end{itemize}
The monad law violations are ``not observable''
\end{frame}

\begin{frame}{Free constructions in mathematics: Example I}
\begin{itemize}
\item Consider the Russian letter ц (ts\`{e}) and the Chinese word \shui~(shu\textipa{\v i})
\item We want to \emph{multiply} ц by \shui. Multiply how?
\item Say, we want an associative (but noncommutative) product of them
\begin{itemize}
\item So we want to define a \emph{semigroup} that \emph{contains} ц and
\shui~as elements
\begin{itemize}
\item while we still know nothing about ц and \shui
\end{itemize}
\end{itemize}
\item Consider the set of all \emph{unevaluated expressions} such as ц$\cdot$\shui$\cdot$\shui$\cdot$ц$\cdot$\shui
\begin{itemize}
\item Here ц$\cdot$\shui~is different from \shui$\cdot$ц but $\left(a\cdot b\right)\cdot c=a\cdot\left(b\cdot c\right)$
\end{itemize}
\item All these expressions form a \textbf{free semigroup} generated by
ц and \shui
\begin{itemize}
\item This is the most unrestricted semigroup that contains ц and \shui
\end{itemize}
\item Example calculation: (\shui$\cdot$\shui)$\cdot$(ц$\cdot$\shui)$\cdot$ц
$=$ \shui$\cdot$\shui$\cdot$ц$\cdot$\shui$\cdot$ц
\end{itemize}
How to represent this as a data type:
\begin{itemize}
\item \textbf{Tree encoding}: the full expression tree: (((\shui,\shui),(ц,\shui)),ц)
\begin{itemize}
\item Implement the operation $a\cdot b$ as pair constructor (easy)
\end{itemize}
\item \textbf{Reduced encoding}, as a ``smart'' structure: List(\shui,\shui,ц,\shui,ц)
\begin{itemize}
\item Implement $a\cdot b$ by concatenating the lists (more expensive)
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Free constructions in mathematics: Example II}
\begin{itemize}
\item Want to define a product operation for $n$-dimensional vectors: $\mathbf{v}_{1}\otimes\mathbf{v}_{2}$
\item The $\otimes$ must be linear and distributive (but not commutative):
\begin{align*}
\mathbf{u}_{1}\otimes\mathbf{v}_{1}+\left(\mathbf{u}_{2}\otimes\mathbf{v}_{2}+\mathbf{u}_{3}\otimes\mathbf{v}_{3}\right) & =\left(\mathbf{u}_{1}\otimes\mathbf{v}_{1}+\mathbf{u}_{2}\otimes\mathbf{v}_{2}\right)+\mathbf{u}_{3}\otimes\mathbf{v}_{3}\\
\mathbf{u}\otimes\left(a_{1}\mathbf{v}_{1}+a_{2}\mathbf{v}_{2}\right) & =a_{1}\left(\mathbf{u}\otimes\mathbf{v}_{1}\right)+a_{2}\left(\mathbf{u}\otimes\mathbf{v}_{2}\right)\\
\left(a_{1}\mathbf{v}_{1}+a_{2}\mathbf{v}_{2}\right) & \otimes\mathbf{u}=a_{1}\left(\mathbf{v}_{1}\otimes\mathbf{u}\right)+a_{2}\left(\mathbf{v}_{2}\otimes\mathbf{u}\right)
\end{align*}

\begin{itemize}
\item We have such a product for 3-dimensional vectors only; ignore that
\end{itemize}
\item Consider \emph{unevaluated} \emph{expressions} of the form $\mathbf{u}_{1}\otimes\mathbf{v}_{1}+\mathbf{u}_{2}\otimes\mathbf{v}_{2}+...$
\begin{itemize}
\item A free vector space generated by pairs of vectors
\end{itemize}
\item Impose the equivalence relationships shown above
\begin{itemize}
\item The result is known as the \textbf{tensor product}
\end{itemize}
\item Tree encoding: full unevaluated expression tree
\begin{itemize}
\item A list of any number of vector pairs $\sum_{i}\mathbf{u}_{i}\otimes\mathbf{v}_{i}$
\end{itemize}
\item Reduced encoding: an $n\times n$ matrix
\begin{itemize}
\item Reduced encoding requires proofs and more complex operations
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Worked example I: Free semigroup}

{\footnotesize{}\vspace{-0.15cm}}Implement a free semigroup \texttt{\textcolor{blue}{\footnotesize{}FSIS}}
generated by two types \texttt{\textcolor{blue}{\footnotesize{}Int}}
and \texttt{\textcolor{blue}{\footnotesize{}String}} 
\begin{itemize}
\item A value of \texttt{\textcolor{blue}{\footnotesize{}FSIS}} can be an
\texttt{\textcolor{blue}{\footnotesize{}Int}}; it can also be a \texttt{\textcolor{blue}{\footnotesize{}String}} 
\item If \texttt{\textcolor{blue}{\footnotesize{}x}}, \texttt{\textcolor{blue}{\footnotesize{}y}}
are of type \texttt{\textcolor{blue}{\footnotesize{}FSIS}} then so
is \texttt{\textcolor{blue}{\footnotesize{}x |+| y}} 
\end{itemize}
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}sealed~trait~FSIS~}\textcolor{darkgray}{\footnotesize{}//~tree~encoding:~full~expression~tree}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Wrap1(x:~Int)~extends~FSIS}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Wrap2(x:~String)~extends~FSIS}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Comb(x:~FSIS,~y:~FSIS)~extends~FSIS}{\footnotesize\par}
\end{lyxcode}
\begin{itemize}
\item {\footnotesize{}\vspace{-0.15cm}}Short type notation: $\text{FSIS}\equiv\text{Int}+\text{String}+\text{FSIS}\times\text{FSIS}$ 
\item For a semigroup $S$ and given $\text{Int}\Rightarrow S$ and $\text{String}\Rightarrow S$,
map $\text{FSIS}\Rightarrow S$
\item Simplify and generalize this construction by setting $Z=\text{Int}+\text{String}$
\begin{itemize}
\item The tree encoding is $\text{FS}^{Z}\equiv Z+\text{FS}^{Z}\times\text{FS}^{Z}$
\end{itemize}
\end{itemize}
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}def~|+|(x:~FS{[}Z{]},~y:~FS{[}Z{]}):~FS{[}Z{]}~=~Comb(x,~y)}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}def~run{[}S:~Semigroup,~Z{]}(extract:~Z~$\Rightarrow$~S):~FS{[}Z{]}~$\Rightarrow$~S~=~\{}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~case~Wrap(z)~$\Rightarrow$~extract(z)}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~case~Comb(x,~y)~$\Rightarrow$~run(extract)(x)~|+|~run(extract)(y)}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}\}~}\textcolor{darkgray}{\footnotesize{}//~Semigroup~laws~will~hold~after~applying~run().}{\footnotesize\par}
\end{lyxcode}
\begin{itemize}
\item {\footnotesize{}\vspace{-0.15cm}}The reduced encoding is $\text{FSR}^{Z}\equiv Z\times\text{List}^{Z}$
(non-empty list of $Z$'s)
\begin{itemize}
\item \texttt{\textcolor{blue}{\footnotesize{}x |+| y}} requires concatenating
the lists, but \texttt{\textcolor{blue}{\footnotesize{}run()}} is
faster
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Worked example II: Free monoid}

{\footnotesize{}\vspace{-0.15cm}}Implement a free monoid \texttt{\textcolor{blue}{\footnotesize{}FM{[}Z{]}}}
generated by type \texttt{\textcolor{blue}{\footnotesize{}Z}} 
\begin{itemize}
\item A value of \texttt{\textcolor{blue}{\footnotesize{}FM{[}Z{]}}} can
be the empty value; it can also be a \texttt{\textcolor{blue}{\footnotesize{}Z}} 
\item If \texttt{\textcolor{blue}{\footnotesize{}x}}, \texttt{\textcolor{blue}{\footnotesize{}y}}
are of type \texttt{\textcolor{blue}{\footnotesize{}FM{[}Z{]}}} then
so is \texttt{\textcolor{blue}{\footnotesize{}x |+| y}} 
\end{itemize}
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}sealed~trait~FM{[}Z{]}~}\textcolor{darkgray}{\footnotesize{}//~tree~encoding}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Empty{[}Z{]}()~extends~FM{[}Z{]}}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Wrap{[}Z{]}(z:~Z)~extends~FM{[}Z{]}}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Comb{[}Z{]}(x:~FM{[}Z{]},~y:~FM{[}Z{]})~extends~FM{[}Z{]}}{\footnotesize\par}
\end{lyxcode}
\begin{itemize}
\item {\footnotesize{}\vspace{-0.15cm}}Short type notation: $\text{FM}^{Z}\equiv1+Z+\text{FM}^{Z}\times\text{FM}^{Z}$ 
\item For a monoid $M$ and given $Z\Rightarrow M$, map $\text{FM}^{Z}\Rightarrow M$
\end{itemize}
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}def~|+|(x:~FM{[}Z{]},~y:~FM{[}Z{]}):~FM{[}Z{]}~=~Comb(x,~y)}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}def~run{[}M:~Monoid,~Z{]}(extract:~Z~$\Rightarrow$~M):~FM{[}Z{]}~$\Rightarrow$~M~=~\{}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~case~Empty()~$\Rightarrow$~Monoid{[}M{]}.empty}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~case~Wrap(z)~$\Rightarrow$~extract(z)}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~case~Comb(x,~y)~$\Rightarrow$~run(extract)(x)~|+|~run(extract)(y)}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}\}~}\textcolor{darkgray}{\footnotesize{}//~Monoid~laws~will~hold~after~applying~run().}{\footnotesize\par}
\end{lyxcode}
\begin{itemize}
\item {\footnotesize{}\vspace{-0.15cm}}The reduced encoding is $\text{FMR}^{Z}\equiv\text{List}^{Z}$
(list of $Z$'s)
\begin{itemize}
\item Implementing \texttt{\textcolor{blue}{\footnotesize{}|+|}} requires
concatenating the lists 
\end{itemize}
\item Reduced encoding and tree encoding give identical results after \texttt{\textcolor{blue}{\footnotesize{}run()}} 
\end{itemize}
\end{frame}

\begin{frame}{Mapping a free semigroup to different targets}

{\footnotesize{}\vspace{-0.15cm}}What if we interpret $\text{FS}^{X}$
into \emph{another} free semigroup?
\begin{itemize}
\item Given $Y\Rightarrow Z$, can we map $\text{FS}^{Y}\Rightarrow\text{FS}^{Z}$?
\begin{itemize}
\item Need to map $\text{FS}^{Y}\equiv Y+\text{FS}^{Y}\times\text{FS}^{Y}\Rightarrow Z+\text{FS}^{Z}\times\text{FS}^{Z}$
\item This is straightforward since $\text{FS}^{X}$ is a functor in $X$:
\end{itemize}
\end{itemize}
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}def~fmap{[}Y,~Z{]}(f:~Y~$\Rightarrow$~Z):~FS{[}Y{]}~$\Rightarrow$~FS{[}Z{]}~=~\{}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~case~Wrap(y)~$\Rightarrow$~Wrap(f(y))}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~case~Comb(a,~b)~$\Rightarrow$~Comb(fmap(f)(a),~fmap(f)(b))}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}\}}{\footnotesize\par}
\end{lyxcode}
\begin{itemize}
\item Now we can use \texttt{\textcolor{blue}{\footnotesize{}run}} to interpret
$\text{FS}^{X}\Rightarrow\text{FS}^{Y}\Rightarrow\text{FS}^{Z}\Rightarrow S$,
etc.
\begin{itemize}
\item Functor laws hold for $\text{FS}^{X}$, so \texttt{\textcolor{blue}{\footnotesize{}fmap}}
is composable as usual
\item The ``interpreter'' commutes with \texttt{\textcolor{blue}{\footnotesize{}fmap}}
as well (naturality law):{\footnotesize{}
\[
\xymatrix{\xyScaleY{0.2pc}\xyScaleX{3pc} & \text{FS}^{Y}\ar[rd]\sp(0.6){\ \text{run}^{S}g^{:Y\Rightarrow S}}\\
\text{FS}^{X}\ar[ru]\sp(0.45){\text{fmap}\,f^{:X\Rightarrow Y}}\ar[rr]\sb(0.5){\text{run}^{S}(f\circ g)^{:X\Rightarrow S}} &  & S
}
\]
}{\footnotesize\par}
\end{itemize}
\item Combine two free semigroups: $\text{FS}^{X+Y}$; inject parts: $\text{FS}^{X}\Rightarrow\text{FS}^{X+Y}$ 
\end{itemize}
\end{frame}

\begin{frame}{Church encoding I: Motivation}
\begin{itemize}
\item {\footnotesize{}\vspace{-0.25cm}}Multiple target semigroups $S_{i}$
require many ``extractors'' $\text{ex}_{i}:Z\Rightarrow S_{i}$
\item Refactor extractors $\text{ex}_{i}$ into evidence of a typeclass
constraint on $S_{i}$
\end{itemize}
\begin{lyxcode}
\textcolor{darkgray}{\footnotesize{}//~Typeclass~ExZ{[}S{]}~has~a~single~method,~extract:~Z~$\Rightarrow$~S.}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}implicit~val~exZ:~ExZ{[}MySemigroup{]}~=~\{~z~$\Rightarrow$~...~\}}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}def~run{[}S:~ExZ~:~Semigroup{]}(fs:~FS{[}Z{]}):~S~=~fs~match~\{}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~case~Wrap(z)~$\Rightarrow$~implicitly{[}ExZ{[}S{]}{]}.extract(z)}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~case~Comb(x,~y)~$\Rightarrow$~run(x)~|+|~run(y)}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}\}}{\footnotesize\par}
\end{lyxcode}
\begin{itemize}
\item {\footnotesize{}\vspace{-0.15cm}}\texttt{\textcolor{blue}{\footnotesize{}run()}}
replaces case classes by fixed functions parameterized by \texttt{\textcolor{blue}{\footnotesize{}S:~ExZ}};
instead we can represent \texttt{\textcolor{blue}{\footnotesize{}FS{[}Z{]}}}
directly by such functions, for example:
\end{itemize}
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}def~wrap{[}S:~ExZ{]}(z:~Z):~S~=~implicitly{[}ExZ{[}S{]}{]}.extract(z)}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}def~x{[}S:~ExZ~:~Semigroup{]}:~S~=~wrap(1)~|+|~wrap(2)}{\footnotesize\par}
\end{lyxcode}
\begin{itemize}
\item The type of \texttt{\textcolor{blue}{\footnotesize{}x}} is {\footnotesize{}$\forall S.\left(Z\Rightarrow S\right)\times\left(S\times S\Rightarrow S\right)\Rightarrow S$};
an equivalent type is{\footnotesize{}
\[
\forall S.\left(\left(Z+S\times S\right)\Rightarrow S\right)\Rightarrow S
\]
}{\footnotesize\par}
\item {\footnotesize{}\vspace{-0.1cm}}This is the ``\textbf{Church encoding}''
(of the free semigroup over $Z$)
\item The Church encoding is based on the theorem {\footnotesize{}$A\cong\forall X.\left(A\Rightarrow X\right)\Rightarrow X$} 
\begin{itemize}
\item this \emph{resembles} the type of the continuation monad, $\left(A\Rightarrow R\right)\Rightarrow R$ 
\item but $\forall X$ makes the function fully generic, like a natural
transformation
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Church encoding II: Disjunction types}
\begin{itemize}
\item {\footnotesize{}\vspace{-0.15cm}}Consider the Church encoding for
the disjunction type $P+Q$ 
\begin{itemize}
\item The encoding is {\footnotesize{}$\forall X.\left(P+Q\Rightarrow X\right)\Rightarrow X\cong\forall X.\left(P\Rightarrow X\right)\Rightarrow\left(Q\Rightarrow X\right)\Rightarrow X$}{\footnotesize\par}
\end{itemize}
\end{itemize}
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}trait~Disj{[}P,~Q{]}~\{~def~run{[}X{]}(cp:~P~$\Rightarrow$~X)(cq:~Q~$\Rightarrow$~X):~X~\}}{\footnotesize\par}
\end{lyxcode}
\begin{itemize}
\item Define some values of this type:
\end{itemize}
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}def~left{[}P,~Q{]}(p:~P)~=~new~Disj{[}P,~Q{]}~\{}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~def~run{[}X{]}(cp:~P~$\Rightarrow$~X)(cq:~Q~$\Rightarrow$~X):~X~=~cp(p)~}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}\}}{\footnotesize\par}
\end{lyxcode}
\begin{itemize}
\item {\footnotesize{}\vspace{-0.1cm}}Now we can implement the analog of
the \texttt{\textcolor{blue}{\footnotesize{}case}} expression simply
as
\end{itemize}
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}val~result~=~disj.run~\{p~$\Rightarrow$~...\}~\{q~$\Rightarrow$~...\}}{\footnotesize\par}
\end{lyxcode}
\begin{itemize}
\item This works in programming languages that have no disjunction types
\end{itemize}
General recipe for implementing the Church encoding: 
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}trait~Blah~\{~def~run{[}X{]}(cont:~...~$\Rightarrow$~X):~X~\}}{\footnotesize\par}
\end{lyxcode}
\begin{itemize}
\item For convenience, define a type class \texttt{\textcolor{blue}{\footnotesize{}Ex}}
describing the inner function:
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}trait~Ex{[}X{]}~\{~def~cp:~P~$\Rightarrow$~X;~def~cq:~Q~$\Rightarrow$~X~\}}{\footnotesize\par}
\end{lyxcode}
\begin{itemize}
\item Different methods of this class return \texttt{\textcolor{blue}{\footnotesize{}X}};
convenient with disjunctions
\end{itemize}
\item Church-encoded types have to be ``run'' for pattern-matching
\end{itemize}
\end{frame}

\begin{frame}{Church encoding III: How it works}

Why is the type $\text{Ch}^{A}\equiv\forall X.\left(A\Rightarrow X\right)\Rightarrow X$
equivalent to the type $A$?
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}trait~Ch{[}A{]}~\{~def~run{[}X{]}(cont:~A~$\Rightarrow$~X):~X~\}}{\footnotesize\par}
\end{lyxcode}
\texttt{\textcolor{blue}{\footnotesize{}}}%
\begin{minipage}[t]{0.65\textwidth}%
\begin{itemize}
\item {\footnotesize{}\vspace{-0.25cm}}If we have a value of $A$, we can
get a $\text{Ch}^{A}$
\end{itemize}
\begin{lyxcode}
{\footnotesize{}\vspace{-0.15cm}}\textcolor{blue}{\footnotesize{}def~a2c{[}A{]}(a:~A):~Ch{[}A{]}~=~new~Ch{[}A{]}~\{~}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}~~def~run{[}X{]}(cont:~A~$\Rightarrow$~X):~X~=~cont(a)}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}\}}{\footnotesize\par}
\end{lyxcode}
\begin{itemize}
\item {\footnotesize{}\vspace{-0.3cm}}If we have a $\text{ch}:\text{Ch}^{A}$,
we can get an $a:A$ 
\end{itemize}
\begin{lyxcode}
{\footnotesize{}\vspace{-0.5cm}}\textcolor{blue}{\footnotesize{}def~c2a{[}A{]}(ch:~Ch{[}A{]}):~A~=~ch.run{[}A{]}(a$\Rightarrow$a)}{\footnotesize\par}
\end{lyxcode}
%
\end{minipage}\texttt{\textcolor{blue}{\footnotesize{}\hfill{}}}%
\begin{minipage}[t]{0.3\columnwidth}%
{\footnotesize{}
\[
\xymatrix{\xyScaleY{1pc}\xyScaleX{3pc}\text{id}:\left(A\Rightarrow A\right)\ar[r]\sp(0.65){\text{ch}.\text{run}^{A}}\ar[d]\sp(0.5){\text{fmap}_{\text{Reader}_{A}}\left(f\right)} & A\ar[d]\sp(0.45){f}\\
f:\left(A\Rightarrow X\right)\ar[r]\sb(0.65){\text{ch}.\text{run}^{X}} & X
}
\]
}%
\end{minipage}\texttt{\textcolor{blue}{\footnotesize{}\hfill{}}}{\footnotesize\par}
\begin{itemize}
\item The functions \texttt{\textcolor{blue}{\footnotesize{}a2c}} and \texttt{\textcolor{blue}{\footnotesize{}c2a}}
are inverses of each other
\begin{itemize}
\item To implement a value $\text{ch}^{:\text{Ch}^{A}}$, we must compute
an $x^{:X}$ given $f^{:A\Rightarrow X}$, for \emph{any} $X$, which
\emph{requires} having a value $a^{:A}$ available
\end{itemize}
\item To show that \texttt{\textcolor{blue}{\footnotesize{}ch = a2c(c2a(ch))}},
apply both sides to an \texttt{\textcolor{blue}{\footnotesize{}f:~A$\Rightarrow$X}}
and get \texttt{\textcolor{blue}{\footnotesize{}ch.run(f) = a2c(c2a(ch)).run(f)
= f(c2a(ch)) = f(ch.run(a$\Rightarrow$a))}} 
\begin{itemize}
\item This is naturality of \texttt{\textcolor{blue}{\footnotesize{}ch.run}}
as a transformation between \texttt{\textcolor{blue}{\footnotesize{}Reader}}
and \texttt{\textcolor{blue}{\footnotesize{}Id}} 
\begin{itemize}
\item Naturality of \texttt{\textcolor{blue}{\footnotesize{}ch.run}} follows
from parametricity of its code
\end{itemize}
\item It is straightforward to compute \texttt{\textcolor{blue}{\footnotesize{}c2a(a2c(a))
= identity(a) = a}} 
\end{itemize}
\item Church encoding satisfies laws: it is built up from parts of \texttt{\textcolor{blue}{\footnotesize{}run}}
method
\end{itemize}
\end{frame}

\begin{frame}{Worked example III: Free functor I}
\begin{itemize}
\item The \texttt{\textcolor{blue}{\footnotesize{}Functor}} type class has
one method, \texttt{\textcolor{blue}{\footnotesize{}fmap}}: $\left(Z\Rightarrow A\right)\Rightarrow F^{Z}\Rightarrow F^{A}$ 
\item The tree encoding of a free functor over $F^{\bullet}$ needs two
case classes:
\end{itemize}
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}sealed~trait~FF{[}F{[}\_{]},~A{]}}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Wrap{[}F{[}\_{]},~A{]}(fa:~F{[}A{]})~extends~FF{[}F,~A{]}}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Fmap{[}F{[}\_{]},~A,~Z{]}(f:~Z~\ensuremath{\Rightarrow}~A)(ffz:~FF{[}F,~Z{]})~extends~FF{[}F,~A{]}}{\footnotesize\par}
\end{lyxcode}
\begin{itemize}
\item {\footnotesize{}\vspace{-0.15cm}}The constructor \texttt{\textcolor{blue}{\footnotesize{}Fmap}}
has an extra type parameter $Z$, which is ``hidden''
\end{itemize}
Consider a simple example of this:
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}sealed~trait~Q{[}A{]};~case~class~QZ{[}A,~Z{]}(a:~A,~z:~Z)~extends~Q{[}A{]}}{\footnotesize\par}
\end{lyxcode}
\begin{itemize}
\item Need to use specific type $Z$ when constructing a value of \texttt{\textcolor{blue}{\footnotesize{}Q{[}A{]}}},
e.g.,
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}val~q:~Q{[}Int{]}~=~QZ{[}Int,~String{]}(123,~\textquotedbl abc\textquotedbl )}{\footnotesize\par}
\end{lyxcode}
\begin{itemize}
\item The type $Z$ is hidden inside $q:Q^{\text{Int}}$; all we know is
that $Z$ ``exists''
\end{itemize}
\item Type notation for this: $Q^{A}\equiv\exists Z.A\times Z$
\begin{itemize}
\item The existential quantifier applies to the ``hidden'' type parameter
\item The constructor \texttt{\textcolor{blue}{\footnotesize{}QZ}} has type
$\exists Z.\left(A\times Z\Rightarrow Q^{A}\right)$
\item It is not $\forall Z$ because a specific $Z$ is used when building
up a value
\item The code does not show $\exists Z$ explicitly! We need to keep track
of that
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Encoding with an existential type: How it works}

Show that $P^{A}\equiv\exists Z.Z\times\left(Z\Rightarrow A\right)\cong A$
\begin{lyxcode}
{\footnotesize{}\vspace{-0.35cm}}\textcolor{blue}{\footnotesize{}sealed~trait~P{[}A{]};~case~class~PZ{[}A,~Z{]}(z:~Z,~f:~Z~$\Rightarrow$~A)~extends~P{[}A{]}}{\footnotesize\par}
\end{lyxcode}
\begin{itemize}
\item {\footnotesize{}\vspace{-0.15cm}}How to construct a value of type
$P^{A}$ for a given $A$?
\begin{itemize}
\item Have a function $Z\Rightarrow A$ and a $Z$, construct $Z\times\left(Z\Rightarrow A\right)$
\item Particular case: $Z\equiv A$, have $a:A$ and build $a\times\text{id}^{:A\Rightarrow A}$
\end{itemize}
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}def~a2p{[}A{]}(a:~A):~P{[}A{]}~=~PZ{[}A,~A{]}(a,~identity)}{\footnotesize\par}
\end{lyxcode}
\item Cannot extract $Z$ out of $P^{A}$ -- the type $Z$ is hidden
\item \emph{Can} extract $A$ out of $P^{A}$ -- do not need to know $Z$
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}def~p2a{[}A{]}:~P{[}A{]}~$\Rightarrow$~A~=~\{~case~PZ(z,~f)~$\Rightarrow$~f(z)~\}}{\footnotesize\par}
\end{lyxcode}
\item Cannot transform $P^{A}$ into anything else other than $A$
\item A value of type $P^{A}$ is observable only via \texttt{\textcolor{blue}{\footnotesize{}p2a}} 
\begin{itemize}
\item Therefore the functions \texttt{\textcolor{blue}{\footnotesize{}a2p}}
and \texttt{\textcolor{blue}{\footnotesize{}p2a}} are ``observational''
inverses (i.e.~we need to use \texttt{\textcolor{blue}{\footnotesize{}p2a}}
in order to compare values of type $P^{A}$)
\end{itemize}
\end{itemize}
{\footnotesize{}\vspace{-0.15cm}}If $F^{\bullet}$ is a functor then
$Q^{A}\equiv\exists Z.F^{Z}\times\left(Z\Rightarrow A\right)\cong F^{A}$
\begin{itemize}
\item A value of $Q^{A}$ can be observed only by extracting an $F^{A}$
from it
\item Can define \texttt{\textcolor{blue}{\footnotesize{}f2q}} and \texttt{\textcolor{blue}{\footnotesize{}q2f}}
and show that they are observational inverses
\end{itemize}
\end{frame}

\begin{frame}{Worked example III: Free functor II}
\begin{itemize}
\item Tree encoding of \texttt{\textcolor{blue}{\footnotesize{}FF}} has
type $\text{FF}^{F^{\bullet},A}\equiv F^{A}+\exists Z.\text{FF}^{F^{\bullet},Z}\times\left(Z\Rightarrow A\right)$
\item Derivation of the reduced encoding:
\begin{itemize}
\item A value of type $\text{FF}^{F^{\bullet},A}$ must be of the form {\footnotesize{}
\[
\exists Z_{1}.\exists Z_{2}...\exists Z_{n}.F^{Z_{n}}\times\left(Z_{n}\Rightarrow Z_{n-1}\right)\times...\times\left(Z_{2}\Rightarrow Z_{1}\right)\times\left(Z_{1}\Rightarrow A\right)
\]
}{\footnotesize\par}
\item The functions $Z_{1}\Rightarrow A$, $Z_{2}\Rightarrow Z_{1}$, etc.,
must be composed associatively
\item The equivalent type is $\exists Z_{n}.F^{Z_{n}}\times\left(Z_{n}\Rightarrow A\right)$
\end{itemize}
\item Reduced encoding: $\text{FreeF}^{F^{\bullet},A}\equiv\exists Z.F^{Z}\times\left(Z\Rightarrow A\right)$
\begin{itemize}
\item Substituted $F^{Z}$ instead of $\text{FreeF}^{F^{\bullet},Z}$ and
eliminated the case $F^{A}$
\item The reduced encoding is non-recursive
\item Requires a proof that this encoding is equivalent to the tree encoding
\item If $F^{\bullet}$ is already a functor, can show $F^{A}\cong\exists Z.F^{Z}\times\left(Z\Rightarrow A\right)$
\end{itemize}
\item Church encoding (starting from the tree encoding): $\text{FreeF}^{F^{\bullet},A}\equiv\forall P^{\bullet}.\left(\forall C.\big(F^{C}+\exists Z.P^{Z}\times\left(Z\Rightarrow C\right)\big)\leadsto P^{C}\right)\Rightarrow P^{A}$
\begin{itemize}
\item The structure of the type expression: $\forall P^{\bullet}.\left(\forall C.(...)^{C}\leadsto P^{C}\right)\Rightarrow P^{A}$
\begin{itemize}
\item Cannot move $\forall C$ or $\exists Z$ to the outside of the type
expression!
\end{itemize}
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Church encoding IV: Recursive types and type constructors}
\begin{itemize}
\item Consider the recursive type {\footnotesize{}$P\equiv Z+P\times P$}
(tree with $Z$-valued leaves)
\begin{itemize}
\item The Church encoding is {\footnotesize{}$\forall X.\left(\left(Z+X\times X\right)\Rightarrow X\right)\Rightarrow X$}{\footnotesize\par}
\item This is \emph{non-recursive}: the inductive use of $P$ is replaced
by $X$
\end{itemize}
\item Generalize to recursive type $P\equiv S^{P}$ where $S^{\bullet}$
is a ``induction functor'':
\begin{itemize}
\item The Church encoding of $P$ is {\footnotesize{}$\forall X.\left(S^{X}\Rightarrow X\right)\Rightarrow X$}{\footnotesize\par}
\begin{itemize}
\item Church encoding of recursive types is non-recursive
\item Example: Church encoding of \texttt{\textcolor{blue}{\footnotesize{}List{[}Int{]}}} 
\end{itemize}
\end{itemize}
\item Church encoding of a type constructor $P^{\bullet}$:
\begin{itemize}
\item Notation: $P^{\bullet}$ is a type function; Scala syntax is \texttt{\textcolor{blue}{\footnotesize{}P{[}\_{]}}} 
\item The Church encoding is {\footnotesize{}$\text{Ch}^{P^{\bullet},A}=\forall F^{\bullet}.\left(\forall X.P^{X}\Rightarrow F^{X}\right)\Rightarrow F^{A}$}{\footnotesize\par}
\item Note: $\forall X.P^{X}\Rightarrow F^{X}$ or $P^{\bullet}\leadsto F^{\bullet}$
resembles a natural transformation
\begin{itemize}
\item Except that $P^{\bullet}$ and $F^{\bullet}$ are not necessarily
functors, so no naturality law
\end{itemize}
\item Example: Church encoding of \texttt{\textcolor{blue}{\footnotesize{}Option{[}\_{]}}} 
\end{itemize}
\item Church encoding of a \emph{recursively} defined type constructor $P^{\bullet}$:
\begin{itemize}
\item Definition: $P^{A}\equiv S^{P^{\bullet},A}$ where $S^{P^{\bullet},A}$
describes the ``induction principle''
\item Notation: {\footnotesize{}$S^{\bullet^{\bullet},A}$} is a higher-order
type function; Scala syntax: \texttt{\textcolor{blue}{\footnotesize{}S{[}\_{[}\_{]},A{]}}} 
\begin{itemize}
\item {\footnotesize{}\vspace{-0.3cm}}Example: $\text{List}^{A}\equiv1+A\times\text{List}^{A}\equiv S^{\text{List}^{\bullet},A}$
where $S^{P^{\bullet},A}\equiv1+A\times P^{A}$ 
\end{itemize}
\item The Church encoding of $P^{A}$ is {\footnotesize{}$\text{Ch}^{P^{\bullet},A}=\forall F^{\bullet}.\big(S^{F^{\bullet}}\leadsto F^{\bullet}\big)\Rightarrow F^{A}$}{\footnotesize\par}
\begin{itemize}
\item The Church encoding of \texttt{\textcolor{blue}{\footnotesize{}List{[}\_{]}}}
is non-recursive
\end{itemize}
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Church encoding V: Type classes}
\begin{itemize}
\item Look at the Church encoding of the free semigroup:{\footnotesize{}
\[
\text{ChFS}^{Z}\equiv\forall X.\left(Z\Rightarrow X\right)\times\left(X\times X\Rightarrow X\right)\Rightarrow X
\]
}{\footnotesize\par}
\item If $X$ is constrained to the \texttt{\textcolor{blue}{\footnotesize{}Semigroup}}
typeclass, we will already have a value {\footnotesize{}$X\times X\Rightarrow X$},
so we can omit it: {\footnotesize{}$\text{ChFS}^{Z}=\forall X^{:\text{Semigroup}}.\left(Z\Rightarrow X\right)\Rightarrow X$}{\footnotesize\par}
\begin{itemize}
\item The ``induction functor'' for ``semigroup over $Z$'' is {\footnotesize{}$\text{SemiG}^{X}\equiv Z+X\times X$}{\footnotesize\par}
\item So the Church encoding is $\forall X.\big(\text{SemiG}^{X}\Rightarrow X\big)\Rightarrow X$
\end{itemize}
\end{itemize}
Generalize to arbitrary type classes:
\begin{itemize}
\item Type class $C$ is defined by its operations{\footnotesize{} $C^{X}\Rightarrow X$}
(with a suitable $C^{\bullet}$)
\begin{itemize}
\item call $C^{\bullet}$ the \textbf{method functor} of the inductive typeclass
$C$
\end{itemize}
\item Tree encoding of ``free $C$ over $Z$'' is recursive, $\text{FreeC}^{Z}\equiv Z+C^{\text{FreeC}^{Z}}$
\item Church encoding is $\text{FreeC}^{Z}\equiv\forall X.\left(Z+C^{X}\Rightarrow X\right)\Rightarrow X$
\begin{itemize}
\item Equivalently, $\text{FreeC}^{Z}\equiv\forall X^{:C}.\left(Z\Rightarrow X\right)\Rightarrow X$
\end{itemize}
\item Laws of the typeclass are satisfied automatically after ``running''
\item Works similarly for type constructors: operations $C^{P^{\bullet},A}\Rightarrow P^{A}$
\item Free typeclass $C$ over $F^{\bullet}$ is $\text{FreeC}^{F^{\bullet},A}\equiv\forall P^{\bullet:C}.\left(F^{\bullet}\leadsto P^{\bullet}\right)\Rightarrow P^{A}$
\end{itemize}
\end{frame}

\begin{frame}{Properties of free type constructions}

Generalizing from our examples so far:
\begin{itemize}
\item We ``enriched'' $Z$ to a monoid $\text{FM}^{Z}$, and $F^{A}$
to a monad $\text{DSL}^{F,A}$ 
\begin{itemize}
\item The ``enrichment'' adds case classes representing the needed operations
\item Works for a generating type $Z$ and for a generating type constructor
$F^{A}$
\end{itemize}
\item Obtain a \textbf{free type construction}, which performs no computations
\begin{itemize}
\item $\text{FM}^{Z}$ wraps $Z$ in ``just enough'' stuff to make it
look like a monoid
\item $\text{FreeF}^{F^{\bullet},A}$ wraps $F^{A}$ in ``just enough''
stuff to make it look like a functor
\end{itemize}
\item A value of a free construction can be ``run'' to yield non-free
values 
\end{itemize}
Questions:
\begin{itemize}
\item Can we construct a free typeclass $C$ over any type constructor $F^{A}$?
\begin{itemize}
\item Yes, with typeclasses: (contra)functor, filterable, monad, applicative
\end{itemize}
\item Which of the possible encodings to use?
\begin{itemize}
\item Tree encoding, reduced encodings, Church encoding
\end{itemize}
\item What are the laws for the{\footnotesize{} $\text{FreeC}^{F,A}$} --
``free instance of $C$ over $F$''?
\begin{itemize}
\item For all $F^{\bullet}$, must have \texttt{\textcolor{blue}{\footnotesize{}wrap{[}A{]}}}
$:F^{A}\Rightarrow\text{FreeC}^{F,A}$ or $F^{\bullet}\leadsto\text{FreeC}^{F,\bullet}$
\item For all $M^{\bullet}:C$, must have \texttt{\textcolor{blue}{\footnotesize{}run}}
$:\left(F^{\bullet}\leadsto M^{\bullet}\right)\Rightarrow\text{FreeC}^{F,\bullet}\leadsto M^{\bullet}$
\item The laws of typeclass $C$ must hold after interpreting into an $M^{\bullet}:C$
\item Given any \texttt{\textcolor{blue}{\footnotesize{}t}}$:F^{\bullet}\leadsto G^{\bullet}$,
must have \texttt{\textcolor{blue}{\footnotesize{}fmap(t)}}$:\text{FreeC}^{F,\bullet}\leadsto\text{FreeC}^{G,\bullet}$
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Recipes for encoding free typeclass instances}
\begin{itemize}
\item Build a free instance of typeclass $C$ over $F^{\bullet}$, as a
type constructor $P^{\bullet}$ 
\begin{itemize}
\item The typeclass $C$ can be functor, contrafunctor, monad, etc.
\end{itemize}
\item Assume that $C$ has methods $m_{1}$, $m_{2}$, ..., with type signatures
{\footnotesize{}$m_{1}:Q_{1}^{P^{\bullet},A}\Rightarrow P^{A}$},
{\footnotesize{}$m_{2}:Q_{2}^{P^{\bullet},A}\Rightarrow P^{A}$},
etc., where $Q_{i}^{P^{\bullet},A}$ are covariant in $P^{\bullet}$ 
\begin{itemize}
\item \textbf{Inductive typeclass} is defined via a methods functor, $S^{P^{\bullet}}\leadsto P^{\bullet}$
\end{itemize}
\item The tree encoded $\text{FC}^{A}$ is a disjunction defined recursively
by{\footnotesize{}
\[
\text{FC}^{A}\equiv F^{A}+Q_{1}^{\text{FC}^{\bullet},A}+Q_{2}^{\text{FC}^{\bullet},A}+...
\]
}{\footnotesize\par}
\begin{lyxcode}
{\footnotesize{}\vspace{-0.35cm}}\textcolor{blue}{\footnotesize{}sealed~trait~FC{[}A{]};~case~class~Wrap{[}A{]}(fa:~F{[}A{]})~extends~FC{[}A{]}}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Q1{[}A{]}(...)~extends~FC{[}A{]}}{\footnotesize\par}

\textcolor{blue}{\footnotesize{}case~class~Q2{[}A{]}(...)~extends~FC{[}A{]};~...}{\footnotesize\par}
\end{lyxcode}
\begin{itemize}
\item Any type parameters within $Q_{i}$ are then existentially quantified
\item \texttt{\textcolor{blue}{\footnotesize{}run()}} maps $F^{\bullet}\leadsto M^{\bullet}$
in the disjunction and recursively for other parts
\end{itemize}
\item Derive a reduced encoding via reasoning about possible values of $\text{FC}^{A}$
and by taking into account the laws of the typeclass $C$
\item A Church encoding can use the tree encoding or the reduced encoding
\begin{itemize}
\item Church encoding is ``automatically reduced'', but performance may
differ
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Properties of inductive typeclasses}

If a typeclass $C$ is inductive with methods $C^{X}\Rightarrow X$
then:
\begin{itemize}
\item A free instance of $C$ over $Z$ can be tree-encoded as {\footnotesize{}$\text{FreeC}^{Z}\equiv Z+C^{\text{FreeC}^{Z}}$} 
\begin{itemize}
\item All inductive typeclasses have free instances, $\text{FreeC}^{Z}$
\end{itemize}
\item If $P^{:C}$ and $Q^{:C}$ then $P\times Q$ and $Z\Rightarrow P$
also belong to typeclass $C$
\begin{itemize}
\item but not necessarily $P+Q$ or $Z\times P$
\item Proof: can implement $(C^{P}\Rightarrow P)\times(C^{Q}\Rightarrow Q)\Rightarrow C^{P\times Q}\Rightarrow P\times Q$
and $\left(C^{P}\Rightarrow P\right)\Rightarrow C^{Z\Rightarrow P}\Rightarrow Z\Rightarrow P$,
but cannot implement $\left(...\right)\Rightarrow P+Q$
\end{itemize}
\item Analogous properties hold for type constructor typeclasses
\begin{itemize}
\item Methods described as $C^{F^{\bullet},A}\Rightarrow F^{A}$ with type
constructor parameter $F^{\bullet}$
\end{itemize}
\end{itemize}
What typeclasses \emph{cannot} be tree-encoded (or have no ``free''
instances)?
\begin{itemize}
\item Any typeclass with a method \emph{not ultimately returning} a value
of $P^{A}$
\begin{itemize}
\item Example: a typeclass with methods $\text{pt}:A\Rightarrow P^{A}$
and $\text{ex}:P^{A}\Rightarrow A$
\end{itemize}
\item Such typeclasses are not inductive
\begin{itemize}
\item Typeclasses with methods of the form $P^{A}\Rightarrow...$ are \textbf{co-inductive}
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Worked example IV: Free contrafunctor}
\begin{itemize}
\item Method $\text{contramap}:C^{A}\times\left(B\Rightarrow A\right)\Rightarrow C^{B}$ 
\item Tree encoding: $\text{FreeCF}^{F^{\bullet},B}\equiv F^{B}+\exists A.\text{FreeCF}^{F^{\bullet},A}\times\left(B\Rightarrow A\right)$
\item Reduced encoding: $\text{FreeCF}^{F^{\bullet},B}\equiv\exists A.F^{A}\times\left(B\Rightarrow A\right)$ 
\begin{itemize}
\item A value of type $\text{FreeCF}^{F^{\bullet},B}$ must be of the form
{\footnotesize{}
\[
\exists Z_{1}.\exists Z_{2}...\exists Z_{n}.F^{Z_{1}}\times\left(B\Rightarrow Z_{n}\right)\times\left(Z_{n}\Rightarrow Z_{n-1}\right)\times...\times\left(Z_{2}\Rightarrow Z_{1}\right)
\]
}{\footnotesize\par}
\item The functions $B\Rightarrow Z_{n}$, $Z_{n}\Rightarrow Z_{n-1}$,
etc., are composed associatively
\item The equivalent type is $\exists Z_{1}.F^{Z_{1}}\times\left(B\Rightarrow Z_{1}\right)$
\end{itemize}
\item The reduced encoding is non-recursive
\item Example: $F^{A}\equiv A$, ``interpret'' into the contrafunctor
$C^{A}\equiv A\Rightarrow\text{String}$
\end{itemize}
\begin{lyxcode}
{\footnotesize{}\vspace{-0.35cm}}\textcolor{blue}{\footnotesize{}def~prefixLog{[}A{]}(p:~A):~A~$\Rightarrow$~String~=~a~$\Rightarrow$~p.toString~+~a.toString}{\footnotesize\par}
\end{lyxcode}
\begin{itemize}
\item If $F^{\bullet}$ is already a contrafunctor then $\text{FreeCF}^{F^{\bullet},A}\cong F^{A}$
\end{itemize}
\end{frame}

\begin{frame}{Worked example V: Free pointed functor}

Over an arbitrary type constructor $F^{\bullet}$:
\begin{itemize}
\item Pointed functor methods {\footnotesize{}$\text{pt}:A\Rightarrow P^{A}$}
and {\footnotesize{}$\text{map}:P^{A}\times\left(A\Rightarrow B\right)\Rightarrow P^{B}$}{\footnotesize\par}
\item Tree encoding: {\footnotesize{}$\text{FreeP}^{F^{\bullet},A}\equiv A+F^{A}+\exists Z.\text{FreeP}^{F^{\bullet},Z}\times\left(Z\Rightarrow A\right)$}{\footnotesize\par}
\item Derivation of the reduced encoding:
\begin{itemize}
\item The tree encoding of a value $\text{FreeP}^{F^{\bullet},A}$ is either{\footnotesize{}
\[
\exists Z_{1}.\exists Z_{2}...\exists Z_{n}.F^{Z_{n}}\times\left(Z_{n}\Rightarrow Z_{n-1}\right)\times...\times\left(Z_{2}\Rightarrow Z_{1}\right)\times\left(Z_{1}\Rightarrow A\right)
\]
}or{\footnotesize{}
\[
\exists Z_{1}.\exists Z_{2}...\exists Z_{n}.Z_{n}\times\left(Z_{n}\Rightarrow Z_{n-1}\right)\times...\times\left(Z_{2}\Rightarrow Z_{1}\right)\times\left(Z_{1}\Rightarrow A\right)
\]
}{\footnotesize\par}
\item Compose all functions by associativity; one function $Z_{n}\Rightarrow A$
remains
\item The case $\exists Z_{n}.Z_{n}\times\left(Z_{n}\Rightarrow A\right)$
is equivalent to just $A$
\end{itemize}
\item Reduced encoding: {\footnotesize{}$\text{FreeP}^{F^{\bullet},A}\equiv A+\exists Z.F^{Z}\times\left(Z\Rightarrow A\right)$,
}non-recursive
\item This reuses the free functor as $\text{FreeP}^{F^{\bullet},A}=A+\text{FreeF}^{F^{\bullet},A}$
\end{itemize}
If the type constructor $F^{\bullet}$ is \emph{already} a functor,
$\text{FreeF}^{F^{\bullet},A}\cong F^{A}$ and so:
\begin{itemize}
\item Free pointed functor over a functor $F^{\bullet}$ is simplified:
$A+F^{A}$
\item If $F^{\bullet}$ is already a pointed functor, need not use the free
construction
\begin{itemize}
\item If we do, we will have $\text{FreeP}^{F^{\bullet},A}\not\cong F^{A}$ 
\item only functors and contrafunctors do not change under ``free''
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Worked example VI: Free filterable functor}
\begin{itemize}
\item (See Chapter 6.) Methods:
\begin{align*}
\text{map} & :F^{A}\Rightarrow\left(A\Rightarrow B\right)\Rightarrow F^{B}\\
\text{mapOpt} & :F^{A}\Rightarrow\left(A\Rightarrow1+B\right)\Rightarrow F^{B}
\end{align*}
\item We can recover \texttt{\textcolor{blue}{\footnotesize{}map}} from
\texttt{\textcolor{blue}{\footnotesize{}mapOpt}}, so we keep only
\texttt{\textcolor{blue}{\footnotesize{}mapOpt}} 
\item Tree encoding: $\text{FreeFi}^{F^{\bullet},A}\equiv F^{A}+\exists Z.\text{FreeFi}^{F^{\bullet},Z}\times\left(Z\Rightarrow1+A\right)$
\begin{itemize}
\item If $F^{\bullet}$ is already a functor, can simplify the tree encoding
using the identity $\exists Z.P^{Z}\times\left(Z\Rightarrow1+A\right)\cong P^{A}$
and obtain $\text{FreeFi}^{F^{\bullet},A}\equiv F^{A}+\text{FreeFi}^{F^{\bullet},1+A}$,
which is equivalent to $\text{FreeFi}^{F^{\bullet},A}=F^{A}+F^{1+A}+F^{1+1+A}+...$
\end{itemize}
\item Reduced encoding: $\text{FreeFi}^{F^{\bullet},A}\equiv\exists Z.F^{Z}\times\left(Z\Rightarrow1+A\right)$,
non-recursive
\begin{itemize}
\item {\footnotesize{}\vspace{-0.35cm}}Derivation: $\exists Z_{1}...\exists Z_{n}.F^{Z_{n}}\times\left(Z_{n}\Rightarrow1+Z_{n-1}\right)\times...\times\left(Z_{1}\Rightarrow1+A\right)$
is simplified using the laws of \texttt{\textcolor{blue}{\footnotesize{}mapOpt}}
and Kleisli composition, and yields $\exists Z_{n}.F^{Z_{n}}\times\left(Z_{n}\Rightarrow1+A\right)$.
Encode $F^{A}$ as $\exists Z.F^{Z}\times\left(Z\Rightarrow0+Z\right)$.
\item If $F^{\bullet}$ is already a functor, the reduced encoding is $\text{FreeFi}^{F^{\bullet},A}=F^{1+A}$
\item Free filterable over a filterable functor $F^{\bullet}$ is not equivalent
to $F^{\bullet}$
\end{itemize}
\item Free filterable contrafunctor is constructed in a similar way
\end{itemize}
\end{frame}

\begin{frame}{Worked example VII: Free monad}
frame}

\begin{frame}{Worked example VII: Free monad}
\begin{itemize}
\item {\footnotesize{}\vspace{-0.25cm}}Methods:{\footnotesize{}\vspace{-0.25cm}}
\begin{align*}
\text{pure} & :A\Rightarrow F^{A}\\
\text{flatMap} & :F^{A}\Rightarrow(A\Rightarrow F^{B})\Rightarrow F^{B}
\end{align*}
\item {\footnotesize{}\vspace{-0.25cm}}Can recover \texttt{\textcolor{blue}{\footnotesize{}map}}
from \texttt{\textcolor{blue}{\footnotesize{}flatMap}} and \texttt{\textcolor{blue}{\footnotesize{}pure}},
so we keep only \texttt{\textcolor{blue}{\footnotesize{}flatMap}} 
\item Tree encoding: {\footnotesize{}$\text{FreeM}^{F^{\bullet},A}\equiv F^{A}+A+\exists Z.\text{FreeM}^{F^{\bullet},Z}\times\big(Z\Rightarrow\text{FreeM}^{F^{\bullet},A}\big)$}{\footnotesize\par}
\item Derivation of reduced encoding: 
\begin{itemize}
\item can simplify $A\times\big(A\Rightarrow\text{FreeM}^{F^{\bullet},B}\big)\cong\text{FreeM}^{F^{\bullet},B}$
\item use associativity to replace $\text{FreeM}^{A}\times(A\Rightarrow\text{FreeM}^{B})\times(B\Rightarrow\text{FreeM}^{C})$
by $\text{FreeM}^{A}\times\big(A\Rightarrow\text{FreeM}^{B}\times(B\Rightarrow\text{FreeM}^{C})\big)$
\item therefore we can replace $\exists Z.\text{FreeM}^{F^{\bullet},Z}\times...$
by $\exists Z.F^{Z}\times...$
\end{itemize}
\item Reduced encoding: $\text{FreeM}^{F^{\bullet},A}\equiv A+\exists Z.F^{Z}\times\big(Z\Rightarrow\text{FreeM}^{F^{\bullet},A}\big)$
\item ``\textbf{Final} \textbf{Tagless} style'' means ``Church encoding
of free monad over $F^{\bullet}$''
\item Free monad over a functor $F^{\bullet}$ is $\text{FreeM}^{F^{\bullet},A}\equiv A+F^{\text{FreeM}^{F^{\bullet},A}}$
\begin{itemize}
\item Free monad $\text{FreeM}^{M^{\bullet},\bullet}$ over a monad $M^{\bullet}$
is not equivalent to $M^{\bullet}$
\end{itemize}
\item Free monad over a pointed functor $F^{\bullet}$ is {\footnotesize{}$\text{FreeM}^{F^{\bullet},A}\equiv F^{A}+F^{\text{FreeM}^{F^{\bullet},A}}$}{\footnotesize\par}
\begin{itemize}
\item start from half-reduced encoding $F^{A}+\exists Z.F^{Z}\times\big(Z\Rightarrow\text{FreeM}^{F^{\bullet},A}\big)$ 
\item replace the existential type by an equivalent type $F^{\text{FreeM}^{F^{\bullet},A}}$
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Worked example VIII: Free applicative functor}
\begin{itemize}
\item {\footnotesize{}\vspace{-0.15cm}}Methods:{\footnotesize{}\vspace{-0.15cm}}
\begin{align*}
\text{pure} & :A\Rightarrow F^{A}\\
\text{ap} & :F^{A}\Rightarrow F^{A\Rightarrow B}\Rightarrow F^{B}
\end{align*}
\item {\footnotesize{}\vspace{-0.15cm}}We can recover \texttt{\textcolor{blue}{\footnotesize{}map}}
from \texttt{\textcolor{blue}{\footnotesize{}ap}} and \texttt{\textcolor{blue}{\footnotesize{}pure}},
so we omit \texttt{\textcolor{blue}{\footnotesize{}map}} 
\item Tree encoding: {\footnotesize{}$\text{FreeAp}^{F^{\bullet},A}\equiv F^{A}+A+\exists Z.\text{FreeAp}^{F^{\bullet},Z}\times\text{FreeAp}^{F^{\bullet},Z\Rightarrow A}$}{\footnotesize\par}
\item Reduced encoding:{\footnotesize{} $\text{FreeAp}^{F^{\bullet},A}\equiv A+\exists Z.F^{Z}\times\text{FreeAp}^{F^{\bullet},Z\Rightarrow A}$}{\footnotesize\par}
\begin{itemize}
\item Derivation: a $\text{FreeAp}^{A}$ is either $\exists Z_{1}...\exists Z_{n}.Z_{1}\times\text{FreeAp}^{Z_{1}\Rightarrow Z_{2}}\times...$
or $\exists Z_{1}...\exists Z_{n}.F^{Z_{1}}\times\text{FreeAp}^{Z_{1}\Rightarrow Z_{2}}\times...$;
encode $Z_{1}\times\text{FreeAp}^{Z_{1}\Rightarrow Z_{2}}$ equivalently
as $\text{FreeAp}^{Z_{1}\Rightarrow Z_{2}}\times\left(\left(Z_{1}\Rightarrow Z_{2}\right)\Rightarrow Z_{2}\right)$
using the identity law; so the first $\text{FreeAp}^{Z}$ is always
$F^{A}$, or we have a pure value 
\end{itemize}
\item Free applicative over a functor $F^{\bullet}$: 
\begin{align*}
\text{FreeAp}^{F^{\bullet},A} & \equiv A+\text{FreeZ}^{F^{\bullet},A}\\
\text{FreeZ}^{F^{\bullet},A} & \equiv F^{A}+\exists Z.F^{Z}\times\text{FreeZ}^{F^{\bullet},Z\Rightarrow A}
\end{align*}

\begin{itemize}
\item $\text{FreeZ}^{F^{\bullet},\bullet}$ is the reduced encoding of ``free
zippable'' (no \texttt{\textcolor{blue}{\footnotesize{}pure}})
\end{itemize}
\item $\text{FreeAp}^{F^{\bullet},\bullet}$ over an applicative functor
$F^{\bullet}$ is not equivalent to $F^{\bullet}$
\end{itemize}
\end{frame}

\begin{frame}{Laws for free typeclass constructions}

Consider an inductive typeclass $C$ with methods $C^{A}\Rightarrow A$

Define a free instance of $C$ over $Z$ recursively, {\footnotesize{}$\text{FreeC}^{Z}\equiv Z+C^{\text{FreeC}^{Z}}$}{\footnotesize\par}
\begin{itemize}
\item $\text{FreeC}^{Z}$ has an instance of $C$, i.e.~we can implement
$C^{\text{FreeC}^{Z}}\Rightarrow\text{FreeC}^{Z}$
\item $\text{FreeC}^{Z}$ is a functor in $Z$; {\footnotesize{}$\text{fmap}_{\text{FreeC}}:\left(Y\Rightarrow Z\right)\Rightarrow\text{FreeC}^{Y}\Rightarrow\text{FreeC}^{Z}$}{\footnotesize\par}
\end{itemize}
{\footnotesize{}\vspace{-0.45cm}}%
\begin{minipage}[t]{0.64\columnwidth}%
\begin{itemize}
\item For a $P^{:C}$ we can implement the functions {\footnotesize{}
\begin{align*}
\text{run}^{P} & :\left(Z\Rightarrow P\right)\Rightarrow\text{FreeC}^{Z}\Rightarrow P\\
\text{wrap} & :Z\Rightarrow\text{FreeC}^{Z}
\end{align*}
}
\end{itemize}
%
\end{minipage}{\footnotesize{}}%
\begin{minipage}[t]{0.36\columnwidth}%
{\footnotesize{}
\[
\xymatrix{\xyScaleY{1.5pc}\xyScaleX{5pc}\text{FreeC}^{Y}\ar[d]\sb(0.45){\text{fmap}\,f^{:Y\Rightarrow Z}}\ar[rd]\sp(0.65){\ \text{run}\left(f\circ g\right)}\\
\text{FreeC}^{Z}\ar[r]\sp(0.5){\text{run}(g^{:Z\Rightarrow P})} & P
}
\]
}%
\end{minipage}\hfill{}

Law 1: {\footnotesize{}$\text{run}\left(\text{wrap}\right)=\text{id}$};
law 2: {\footnotesize{}$\text{fmap}\,f\circ\text{run}\,g=\text{run}\left(f\circ g\right)$}
(naturality of \texttt{\textcolor{blue}{\footnotesize{}run}})
\begin{itemize}
\item For any $P^{:C},Q^{:C},g^{:Z\Rightarrow P}$, and a typeclass-preserving
$f^{:P\Rightarrow Q}$, we have{\footnotesize{}
\[
\text{run}^{P}(g)\circ f=\text{run}^{Q}\left(g\circ f\right)\quad\quad\text{– “universal property” of }\text{run}
\]
\[
\xymatrix{\xyScaleY{2.0pc}\xyScaleX{3pc}\text{FreeC}^{Z}\ar[d]\sb(0.4){\text{run}^{P}(g^{:Z\Rightarrow P})}\ar[rd]\sp(0.55){\quad\text{run}^{Q}(g\circ f)} &  &  & C^{P}\ar[d]\sb(0.4){\text{fmap}_{S}f}\ar[r]\sp(0.5){\text{ops}_{P}} & P\ar[d]\sb(0.4){f}\\
P\ar[r]\sp(0.5){f^{:P\Rightarrow Q}} & Q &  & C^{Q}\ar[r]\sp(0.5){\text{ops}_{Q}} & Q
}
\]
}{\footnotesize\par}
\item $f^{:P\Rightarrow Q}$ \textbf{preserves typeclass} $C$ if the diagram
on the right commutes
\end{itemize}
\end{frame}

\begin{frame}{Combining the generating constructors in a free typeclass}
\begin{itemize}
\item Consider $\text{FreeC}^{Z}$ for an inductive typeclass $C$ with
methods $C^{X}\Rightarrow X$
\item We would like to combine generating constructors $Z_{1}$, $Z_{2}$,
etc.
\begin{itemize}
\item In a monadic DSL -- combine different operations defined separately
\begin{itemize}
\item Note: monads do not compose in general
\end{itemize}
\end{itemize}
\item To combine generators, use $\text{FreeC}^{Z_{1}+Z_{2}}$; an ``instance
over $Z_{1}$ and $Z_{2}$''
\begin{itemize}
\item but need to inject parts into disjunction, which is cumbersome
\end{itemize}
\item Church encoding makes this easier to manage:
\begin{itemize}
\item {\footnotesize{}$\text{FreeC}^{Z}\equiv\forall X.\left(Z\Rightarrow X\right)\times\big(C^{X}\Rightarrow X\big)\Rightarrow X$}
and then {\footnotesize{}
\[
\text{FreeC}^{Z_{1}+Z_{2}}\equiv\forall X.\left(Z_{1}\Rightarrow X\right)\times\left(Z_{2}\Rightarrow X\right)\times\big(C^{X}\Rightarrow X\big)\Rightarrow X
\]
}{\footnotesize\par}
\item Encode the functions $Z_{i}\Rightarrow X$ via typeclasses \texttt{\textcolor{blue}{\footnotesize{}ExZ1}},
\texttt{\textcolor{blue}{\footnotesize{}ExZ2}}, etc., where typeclass
\texttt{\textcolor{blue}{\footnotesize{}ExZ1}} has method $Z_{1}\Rightarrow X$,
etc.
\item Then {\footnotesize{}
\[
\text{FreeC}^{Z_{1}+Z_{2}}=\forall X^{:E_{Z_{1}}:E_{Z_{2}}}.\big(C^{X}\Rightarrow X\big)\Rightarrow X
\]
}or equivalently{\footnotesize{}
\[
\text{FreeC}^{Z_{1}+Z_{2}}=\forall X^{:C~:E_{Z_{1}}:E_{Z_{2}}}.X
\]
}{\footnotesize\par}
\item The code is easier to maintain
\end{itemize}
\item This works for all typeclasses $C$ and any number of generators $Z_{i}$
\end{itemize}
\end{frame}

\begin{frame}{Combining different free typeclasses}

\vspace{-0.15cm}To combine free instances of different typeclasses
$C_{1}$ and $C_{2}$:
\begin{itemize}
\item Option 1: use functor composition, $\text{FreeC}_{12}^{Z}\equiv\text{FreeC}_{1}^{\text{FreeC}_{2}^{Z}}$
\begin{itemize}
\item Order of composition matters!
\item Operations of $C_{2}$ need to be lifted into $C_{1}$
\item Works only for inductive typeclasses
\item Encodes $C_{1}^{C_{2}}$ but not $C_{2}^{C_{1}}$
\end{itemize}
\item Option 2: use disjunction of method functors, $C^{X}\equiv C_{1}^{X}+C_{2}^{X}$,
and build the free typeclass instance using $C^{X}$
\begin{itemize}
\item Church encoding: $\text{FreeC}_{12}^{Z}\equiv\forall X.\left(Z\Rightarrow X\right)\times\big(C_{1}^{X}+C_{2}^{X}\Rightarrow X\big)\Rightarrow X$
\end{itemize}
\item Example 1: $C_{1}$ is functor, $C_{2}$ is contrafunctor
\begin{itemize}
\item Interpret a free functor/contrafunctor into a profunctor
\end{itemize}
\item Example 2: $C_{1}$ is monad, $C_{2}$ is applicative functor
\begin{itemize}
\item Interpret into a monad that has a non-standard \texttt{\textcolor{blue}{\footnotesize{}zip}}
implementation
\item Example: interpret into \texttt{\textcolor{blue}{\footnotesize{}Future}}
and convert \texttt{\textcolor{blue}{\footnotesize{}zip}} into parallel
execution
\item Each \texttt{\textcolor{blue}{\footnotesize{}zip}} creates parallel
branch, each \texttt{\textcolor{blue}{\footnotesize{}flatMap}} creates
sequential chain
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Exercises}
\begin{enumerate}
\item {\footnotesize{}\vspace{-0.2cm}Implement a free semigroup generated
by a type $Z$ in the tree encoding and in the reduced encoding. Show
that the semigroup laws hold for the reduced encoding but not for
the tree encoding before interpreting into a lawful semigroup $S$.}{\footnotesize\par}
\item {\footnotesize{}Type $P$ is of typeclass $\text{Mod}_{L}$ (called
``$L$-module'') if a fixed monoid $L$ ``acts'' on $P$ via }\texttt{\textcolor{blue}{\footnotesize{}act}}{\footnotesize{}$:L\Rightarrow P\Rightarrow P$,
with laws $\text{act}\,x\circ\text{act}\,y=\text{act}\left(x\circ y\right)$
and $\text{act}\left(1^{:L}\right)=\text{id}$. Show that $\text{Mod}_{L}$
is an inductive typeclass. Implement a free $L$-module over a type
$Z$. }{\footnotesize\par}
\item {\footnotesize{}Implement a monadic DSL with operations }\texttt{\textcolor{blue}{\footnotesize{}put}}{\footnotesize{}$:A\Rightarrow1$
and }\texttt{\textcolor{blue}{\footnotesize{}get}}{\footnotesize{}$:A$;
run examples. }{\footnotesize\par}
\item {\footnotesize{}Implement the Church encoding of the type constructor
$P^{A}\equiv\text{Int}+A\times A$. For the resulting type constructor,
implement a }\texttt{\textcolor{blue}{\footnotesize{}Functor}}{\footnotesize{}
instance.}{\footnotesize\par}
\item {\footnotesize{}Describe the monoid type class via a method functor
$C^{\bullet}$ (such that the monoid's operations are combined into
the type $S^{M}\Rightarrow M$). Using $S^{\bullet}$, implement the
free monoid over a type $Z$ in the Church encoding.}{\footnotesize\par}
\item {\footnotesize{}Assuming that $F^{\bullet}$ is a functor, define
$Q^{A}\equiv\exists Z.F^{Z}\times\left(Z\Rightarrow A\right)$ and
implement }\texttt{\textcolor{blue}{\footnotesize{}f2q}}{\footnotesize{}$:F^{A}\Rightarrow Q^{A}$
and }\texttt{\textcolor{blue}{\footnotesize{}q2f}}{\footnotesize{}$:Q^{A}\Rightarrow F^{A}$.
Show that these functions are natural transformations, and that they
are inverses of each other ``observationally'', i.e.~after applying
}\texttt{\textcolor{blue}{\footnotesize{}q2f}}{\footnotesize{} in
order to compare values of $Q^{A}$.}{\footnotesize\par}
\item {\footnotesize{}Show: $\forall X.X=0$; $\exists Z.Z\cong1$; $\exists Z.Z\times A\cong A$;
$\forall A.\left(A\times A\times A\Rightarrow A\right)\cong1+1+1$.}{\footnotesize\par}
\item {\footnotesize{}Derive a reduced encoding for a free applicative functor
over a pointed functor.}{\footnotesize\par}
\item {\footnotesize{}Implement a ``free pointed filterable'' typeclass
(combining pointed and filterable) over a type constructor $F^{\bullet}$
in the tree encoding. Derive a reduced encoding. Simplify these encodings
when $F^{\bullet}$ is already a functor.}{\footnotesize\par}
\end{enumerate}
\end{frame}

\begin{frame}{Corrections}
\begin{enumerate}
\item {\footnotesize{}The slides say that the ``universal property'' of
the runner is $\text{run}^{P}g\circ f=\text{run}^{Q}\left(g\circ f\right)$,
however, this is not true; it is the right naturality property of
$\text{run}^{P}:\left(Z\Rightarrow P\right)\Rightarrow\text{FreeC}^{Z}\Rightarrow P$
with respect to the type parameter $P$. The universal property is
$f=\text{wrap}\circ\text{run}^{P}f$ for any $f:Z\Rightarrow P$ and
any type $P$ that belongs to the typeclass $C$.}{\footnotesize\par}
\end{enumerate}
\end{frame}

\end{document}
